M:System.
(l:IdLnk, tg:Id. M(source(l)).dout(l,tg)  M(destination(l)).din(l,tg))
 (i:Id. finite-type({l:IdLnk| destination(l) = i & M(source(l)) sends on link l }))
 M  {D:Dsys| Feasible(D) } 

latex

Definitions	x:A. B(x), System, P  Q, P & Q, t  T, Dsys, Feasible(D), M(i), Prop
Lemmas	d-feasible wf, Id wf, finite-type wf, IdLnk wf, ldst wf, assert wf, ma-sends-on wf, lsrc wf, ma-dout wf, ma-din wf, msga wf, ma-feasible wf